$\forall$$T$:Type, $x$, $y$, $z$:$T$. $\neg$$y$ $=$ $z$ $\Rightarrow$ (($x$ $=$ $y$ $\Rightarrow$ $x$ $=$ $z$) $\Leftrightarrow$ $\neg$$x$ $=$ $y$)